package model.cnf;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.Scanner;

/**
 * represent a clause in a CNF
 * @author stephane
 *
 */
public class Clause{

    private List<Literal> literals;

    public Clause(String line){
    	literals = new ArrayList<Literal>();
    	
    	int i = 0;
    	Scanner sc = new Scanner(line);
		while((i = sc.nextInt()) != 0){
			literals.add(new Literal(i));
		}
    	
    	//cleanClause();
    }
    
    public Clause(List<Literal> list){
    	literals=new ArrayList<Literal>(list);
    	//cleanClause();
    }

    public Clause(Collection<Literal> lit, boolean cleanClause){
    	literals=new ArrayList<Literal>(lit);
    	if(cleanClause) 
    		cleanClause();
    }
	

    /* remove dupplicate literals, etc. 
      return true if the clause is still meaningfull (no tautological, etc.) */
    public boolean cleanClause(){
    	//TODO
    	return true;
    }

    public String toString(){
    	StringBuffer s=new StringBuffer();
    	for(Literal l : literals){
    		s.append(l.toString());
    		s.append(" ");
    	}
    	return s.toString();
    }

    public Literal getLiteral(int i){return literals.get(i);}   
    public boolean isUnit(){return (literals.size()==1);}
    public boolean isBinary(){return (literals.size()==2);}
    public int size(){ return literals.size();}
    
}